﻿using System;
using System.Collections.Generic;

using CoreDES.Utils;
using MBT.Modeling;
using MBT.TestStateLevel;

namespace MBT
{
    /// <summary>
    /// State Space generation for test models
    /// </summary>
    public class TA_Generator 
    {
        public enum FinishReason
        {
            TimeExceed,
            ConditionError,
            CompileError,
            SimulationError,
            UserRequest,
            StateSpaceSizeViolation
        }

        #region -=[ CONFIG ]=-
        public static bool performSafetyAnalysis = true;
        public static bool performLivenessAnalysis = false;
        public static bool performStateSkip = true;
        public static bool performTransitionSkip = false;
        public static bool limitNumberOfStates = true;
        public static bool limitTimeOfComputation = false;
        public static int MAX_NUM_STATES = 10000;
        public static int maximumTimeOfProssesing = 10000;
        #endregion
		
        TestModel mysdes;
        object modelassembelly = null;
        TestAutomaton ss;
        FinishReason reason;


        /// <summary>
        /// Constructor
        /// </summary>
        /// <param name="model"></param>
        public TA_Generator(TestModel model)
        {
            this.mysdes = model;
        }
		
		

        public FinishReason whyFinished
        {
            get
            {
                return reason;
            }
        }


        /// <summary>
        /// Generate state space (without any mask): used for offline testing
        /// </summary>
        /// <returns></returns>
        public TestAutomaton GenerateStateSpace()
        {
            return GenerateStateSpace(null);
        }


        /// <summary>
        /// Generate state space using composition technique (intersection with anothe state space): used for offline testing
        /// </summary>
        /// <param name="mask"></param>
        /// <returns></returns>
        public TestAutomaton GenerateStateSpace(TestAutomaton mask)
        {

            ss = new TestAutomaton();

            Queue<TA_State> maskStateList = new Queue<TA_State>();
            bool useMask = (mask != null);

            int numberOfGeneratedStates = 0;

            ss.Initialize(mysdes.GetCurrentState());

            //Use the mask 
            if (useMask)
                maskStateList.Enqueue((TA_State)mask.GetStates()[0]);
            int lastState = 1;

            for (int i = 0; i < ss.Size; i++)
            {
                TA_State state = (TA_State)ss[i];
                TA_State maskState = null;

                //Use the mask 
                if (useMask)
                    maskState = maskStateList.Dequeue();


                mysdes.SetCurrentState(state.state);

                //List<EnGine.Formalism.EventsCollection4Test.Event> myevent = new List<EventsCollection.Event>();
                //bool hasinstant = false;
                foreach (TestEvent e in mysdes.Events)//myevent)
                {
                    //Check Maximum number of states
                    if (limitNumberOfStates)
                    {
                        numberOfGeneratedStates = ss.Size;
                        if (numberOfGeneratedStates > MAX_NUM_STATES)
                        {
                            reason = FinishReason.StateSpaceSizeViolation;
                            return ss;
                        }
                    }
                    //Check Maximum time of simulation
                    //***** To Do ********************
                    if (limitTimeOfComputation)
                    {

                    }

                    //Count number of possible instances due to parameters
                    int numberOfActionInstance = e.XGenerateDomains(); //mysdes.GenerateDomains(e);
                    for (int instanceID = 0; instanceID < numberOfActionInstance; instanceID++)
                    {
                        //[To Do:] WHy????]
                        mysdes.SetCurrentState(state.state);
                        //bin.GetType().InvokeMember(
                        //        "CurrentState", BindingFlags.SetProperty,
                        //             null, bin, new object[] { state.state });
                        try
                        {
                            if (e.evaluatePreconditionForEachParameter)
                            {

                                if (!e.XRunPreconditionHandler(instanceID) /*mysdes.RunPreconditionHandler(e, instanceID)*//*e.RunPreconditionHandler(instanceID)*/)
                                    continue;
                            }
                            else
                            {
                                if (instanceID == 0)
                                {
                                    if (!e.XRunPreconditionHandler(instanceID) /*mysdes.RunPreconditionHandler(e, instanceID)*/)
                                    {
                                        //Event is disabled for all parameters!
                                        instanceID = numberOfActionInstance;
                                        continue;
                                    }
                                }
                            }
                        }
                        catch(Exception exp)
                        {
                            //System.Windows.Forms.MessageBox.Show("Error in precondition of \"" + e.ID + "\"");
                           Console.WriteLine("Error in execution of \"" + e.ID + "\""+exp);
								return null;
                        }

                        //Use the mask 
                        if (useMask)
                            if (!maskState.HasTransition(e.ID) && e.isControllable)
                                continue;



                        //ActionInfo param = e.RunActionHandler(instanceID);


                        #region support non-deterministic choice
                        //first, call 'reset'
                        Choice.Reset();
                        int callInstance = 0;
                        int numberOfChoices = 0;
                        ActionInfo param = null;
                        while (true)
                        {
                            try
                            {
                                if (callInstance == 0)
                                {
                                    //* then, for the first time, call action instance
                                    param = e.XRunActionHandler(instanceID);
                                    callInstance++;
                                }
                                else
                                {
                                    if (callInstance == 1)
                                    {
                                        if (!Choice.isCalled)
                                            break;
                                        numberOfChoices = Choice.numberOfChoices;
                                    }
                                    if (callInstance == numberOfChoices)
                                        break;

                                    //* each time, before calling action instance:
                                    Choice.NextRound();
                                    param = e.XRunActionHandler(instanceID);
                                    callInstance++;
                                }
                            }
                            catch(Exception exp)
                            {
                                Console.WriteLine("Error in execution of \"" + e.ID + "\""+exp);
								return null;
                            }
                            //* Check if we have to skip this state
                            if (performStateSkip)
                            {
                                bool skip = mysdes.SkipCurrentState();
                                if (skip) continue;
                            }

                            //check that if this state is valid
                            if (performSafetyAnalysis)
                            {
                                try
                                {
                                    mysdes.ValidateCurrentState();
                                }
                                catch
                                {
									Console.WriteLine("Error in state space exploration: The state is not valid!");
                                    return null;
                                }
                            }
                            //check if this state is a final (acceptable) state
                            //bool final = mysdes.isFinalState();

                            object newStateObject = mysdes.GetCurrentState();
                            TA_State newState =
                                ss.AddState(state, newStateObject, new TA_State.TA_Transition(state, e.ID, e.isControllable, param));

                            //Use the mask 
                            if (useMask)
                            {
                                if (newState.id > lastState)
                                {
                                    if (e.isControllable)
                                        maskStateList.Enqueue(maskState.next(e.ID));
                                    else
                                        maskStateList.Enqueue(maskState);
                                    lastState = newState.id;
                                }
                            }
                        }
                        #endregion
                    }
                }

            }

            return ss;
        }


        //public void TestOntheFly(StateSpaceSet mask)
        //{
        //    Utility.mode = Mode.StateSpaceGeneration;
        //    CompileCode(model);
        //    if (modelassembelly == null)
        //    {
        //        MessageBox.Show("Compile Error!");
        //        //return null;
        //    }
        //    object bin = modelassembelly;
        //    ss = new StateSpaceSet();

        //    //List<State> maskState = new List<State>();
        //    Queue<State> maskStateList = new Queue<State>();
        //    bool useMask = (mask != null);

        //    model.Variables.RunInitializer();
        //    int numberOfGeneratedStates = 0;

        //    ss.Initialize(bin.GetType().InvokeMember(
        //                "CurrentState", BindingFlags.GetProperty,
        //                     null, bin, null));

        //    //Use the mask 
        //    if (useMask)
        //        maskStateList.Enqueue(mask.states[0]);
        //    int lastState = 1;

        //    for (int i = 0; i < ss.Count; i++)
        //    {

        //        State state = ss[i];
        //        State maskState = null;

        //        //Use the mask 
        //        if (useMask)
        //            maskState = maskStateList.Dequeue();

        //        bin.GetType().InvokeMember(
        //                "CurrentState", BindingFlags.SetProperty,
        //                     null, bin, new object[] { state.state });

        //        //List<EnGine.Formalism.EventsCollection4Test.Event> myevent = new List<EventsCollection.Event>();
        //        //bool hasinstant = false;
        //        foreach (EnGine.Formalism.EventsCollection4Test.Event e in model.Events)//myevent)
        //        {
        //            //Check Maximum number of states
        //            if (limitNumberOfStates)
        //            {
        //                numberOfGeneratedStates = ss.states.Count;
        //                if (numberOfGeneratedStates > MAX_NUM_STATES)
        //                {
        //                    reason = FinishReason.StateSpaceSizeViolation;
        //                    //return ss;
        //                }
        //            }
        //            //Check Maximum time of simulation
        //            //***** To Do ********************
        //            if (limitTimeOfComputation)
        //            {

        //            }

        //            //Count number of possible instances due to parameters
        //            int numberOfActionInstance = e.RunNumberOfActionInstancesHandler();
        //            for (int instanceID = 0; instanceID < numberOfActionInstance; instanceID++)
        //            {
        //                bin.GetType().InvokeMember(
        //                        "CurrentState", BindingFlags.SetProperty,
        //                             null, bin, new object[] { state.state });
        //                if (e.evaluatePreconditionForEachParameter)
        //                {
        //                    if (!e.RunPreconditionHandler(instanceID)) continue;
        //                }
        //                else
        //                {
        //                    if (instanceID == 0)
        //                    {
        //                        if (!e.RunPreconditionHandler(instanceID))
        //                        {
        //                            //Event is disabled for all parameters!
        //                            instanceID = numberOfActionInstance;
        //                            continue;
        //                        }
        //                    }
        //                }

        //                //Use the mask 
        //                if (useMask)
        //                    if (!maskState.transitionIsEnabled(e.ID) && e._isControllable)
        //                        continue;

        //                ActionInfo param = e.RunActionHandler(instanceID);


        //                //Check if we have to skip this state
        //                if (performStateSkip)
        //                {
        //                    bool skip = (bool)bin.GetType().InvokeMember(
        //                            "skipState", BindingFlags.InvokeMethod,
        //                                 null, bin, null);
        //                    if (skip) continue;
        //                }

        //                //check that if this state is valid
        //                if (performSafetyAnalysis)
        //                {
        //                    try
        //                    {
        //                        bin.GetType().InvokeMember(
        //                            "ValidateCurrentState", BindingFlags.InvokeMethod,
        //                                 null, bin, null);
        //                    }
        //                    catch (Exception exp)
        //                    {
        //                        //Unhandle Exception
        //                        MessageBox.Show(exp.InnerException.ToString(), "Error in generating state-space");
        //                        //return null;
        //                    }
        //                }
        //                //check if this state is a final (acceptable) state
        //                bool final = (bool)bin.GetType().InvokeMember("isFinalState", BindingFlags.InvokeMethod, null, bin, null);

        //                object newStateObject = bin.GetType().InvokeMember("CurrentState", BindingFlags.GetProperty, null, bin, null);
        //                State newState = ss.Add(state, newStateObject, e.ID, e._isControllable, final, param);

        //                //Use the mask 
        //                if (useMask)
        //                {
        //                    if (newState.i > lastState)
        //                    {
        //                        if (e._isControllable)
        //                            maskStateList.Enqueue(maskState.next(e.ID));
        //                        else
        //                            maskStateList.Enqueue(maskState);
        //                        lastState = newState.i;
        //                    }
        //                }

        //            }
        //        }

        //    }
        //    ss.model = model;
        //    //return ss;

        //}



        #region IGenerator Members


        public object Generate()
        {
            return GenerateStateSpace();
        }

        public bool Validate()
        {
            return (modelassembelly != null);
        }


        public bool Compile()
        {
            return true;
        }

        #endregion
    }
}
